diff options
| author | Pierre-Marie Pédrot | 2017-09-04 21:55:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-04 22:15:54 +0200 |
| commit | 01a3776cb801ed6cbeba895d04f75e62fd6f091a (patch) | |
| tree | 66c4c6e7304ec4e92e7dcafbbb7b26978c2bb27a /src/tac2quote.ml | |
| parent | 0012f73a1822b97dd8bc8963bc77490cde83e89f (diff) | |
More notations for primitive tactics.
Diffstat (limited to 'src/tac2quote.ml')
| -rw-r--r-- | src/tac2quote.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/tac2quote.ml b/src/tac2quote.ml index d38d7414fe..ed4cef2e2a 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -191,7 +191,7 @@ let of_clause (loc, cl) = std_proj "on_concl", concl; ]) -let of_destruction_arg ?loc = function +let of_destruction_arg (loc, arg) = match arg with | QElimOnConstr c -> let arg = thunk (of_constr_with_bindings c) in std_constructor ?loc "ElimOnConstr" [arg] @@ -199,7 +199,7 @@ let of_destruction_arg ?loc = function | QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int n] let of_induction_clause (loc, cl) = - let arg = of_destruction_arg ?loc cl.indcl_arg in + let arg = of_destruction_arg cl.indcl_arg in let eqn = of_option ?loc of_intro_pattern_naming cl.indcl_eqn in let as_ = of_option ?loc of_or_and_intro_pattern cl.indcl_as in let in_ = of_option ?loc of_clause cl.indcl_in in |