diff options
Diffstat (limited to 'contrib/subtac/subtac_pretyping.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 0e987cf2..ad76bdeb 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 11047 2008-06-03 23:08:00Z msozeau $ *) +(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Global open Pp @@ -117,7 +117,6 @@ let env_with_binders env isevars l = in aux (env, []) l let subtac_process env isevars id bl c tycon = -(* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *) let c = Command.abstract_constr_expr c bl in let tycon = match tycon with @@ -132,12 +131,14 @@ let subtac_process env isevars id bl c tycon = let imps = Implicit_quantifiers.implicits_of_rawterm c in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars (evars_of !isevars) in - evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps + let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in + evm, coqc, ty, imps open Subtac_obligations let subtac_proof kind env isevars id bl c tycon = let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in - let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in - let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in + let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in + let evm' = Subtac_utils.evars_of_term evm evm' coqt in + let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in add_definition id def ty ~implicits:imps ~kind:kind evars |