diff options
Diffstat (limited to 'src/Conversion_tactics.v')
| -rw-r--r-- | src/Conversion_tactics.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v index 37a39b5..4a791e6 100644 --- a/src/Conversion_tactics.v +++ b/src/Conversion_tactics.v @@ -102,7 +102,7 @@ Ltac converting := repeat match goal with (* On capture chaque sous-terme x avec son contexte, i.e. le but est C[x] *) - | |- appcontext C[?x] => + | |- context C[?x] => (* Si x est de type T *) let U := type of x in lazymatch eval fold T in U with @@ -116,7 +116,7 @@ Ltac converting := pose proof x as var; (* Sinon, on analyse la formule obtenue en remplaçant x par notre variable fraîche dans le but *) lazymatch context C[var] with - | appcontext [?h var] => + | context [?h var] => let h := get_head h in lazymatch h with (* x est déjà réécrit *) @@ -201,7 +201,7 @@ Ltac renaming := repeat match goal with (* S'il y a un terme de la forme (T2Z (f t1 ... tn)) *) - | |- appcontext [T2Z ?X] => + | |- context [T2Z ?X] => (* On récupère le symbole de tête *) let f := get_head X in (* S'il s'agit d'un constructeur on ne fait rien *) @@ -214,7 +214,7 @@ Ltac renaming := repeat match goal with (* Pour chaque terme de la forme (T2Z (f' t'1 ... t'n)) *) - | |- appcontext [T2Z ?X'] => + | |- context [T2Z ?X'] => (* On récupère le symbole de tête *) let f' := get_head X' in (* Si f' = f *) @@ -269,7 +269,7 @@ Ltac renaming' := repeat match goal with (* S'il y a un terme de la forme (f t1 ... (Z2T tn)) *) - | |- appcontext [?X (Z2T ?Y)] => + | |- context [?X (Z2T ?Y)] => (* On récupère le symbole de tête *) let f := get_head X in (* S'il s'agit d'un constructeur on ne fait rien *) @@ -280,7 +280,7 @@ Ltac renaming' := repeat match goal with (* Pour chaque terme de la forme (f' t'1 ... (Z2T t'n)) *) - | |- appcontext [?X' (Z2T ?Y')] => + | |- context [?X' (Z2T ?Y')] => (* On récupère le symbole de tête *) let f' := get_head X' in (* Si f' = f *) |