diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-13 12:49:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-13 12:49:54 +0200 |
| commit | f3b84cf63c242623bdcccd30c536e55983971da5 (patch) | |
| tree | 740984c577ed75c76edc2525b3de9bf744da3c21 /pretyping/evarsolve.ml | |
| parent | b68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (diff) | |
| parent | 9f723f14e5342c1303646b5ea7bb5c0012a090ef (diff) | |
Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contains evars
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 96d80741a..0c109b026 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1592,14 +1592,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = Id.Set.subset (collect_vars evd rhs) !names in let body = - if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *) + if fast rhs then nf_evar evd rhs (** FIXME? *) else let t' = imitate (env,0) rhs in if !progress then (recheck_applications conv_algo (evar_env evi) evdref t'; t') else t' in (!evdref,body) - + (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, * [define] tries to find an instance lhs such that |