From 7e2f953c3c19904616c43990fada92e762aadec9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 29 Jun 2010 08:27:03 +0000 Subject: Made tclABSTRACT normalize evars before saying it does not support them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/subtac/subtac_cases.ml | 6 +++--- plugins/subtac/subtac_classes.ml | 4 ++-- plugins/subtac/subtac_coercion.ml | 4 ++-- plugins/subtac/subtac_command.ml | 12 ++++++------ plugins/subtac/subtac_pretyping.ml | 2 +- 5 files changed, 14 insertions(+), 14 deletions(-) (limited to 'plugins') diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 29ce9d3d4a..491b44fbba 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1894,7 +1894,7 @@ let liftn_rel_context n k sign = liftrec (k + rel_context_length sign) sign let nf_evars_env sigma (env : env) : env = - let nf t = nf_isevar sigma t in + let nf t = nf_evar sigma t in let env0 : env = reset_context env in let f e (na, b, t) e' : env = Environ.push_named (na, Option.map nf b, nf t) e' @@ -1912,7 +1912,7 @@ let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon match rtntyp with | Some rtntyp -> let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in - let predccl = (j_nf_isevar !isevars predcclj).uj_val in + let predccl = (j_nf_evar !isevars predcclj).uj_val in Some (build_initial_predicate true allnames predccl) | None -> match valcon_of_tycon tycon with @@ -1993,7 +1993,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = nf_isevar !isevars tycon; } + uj_type = nf_evar !isevars tycon; } in j else (* We build the elimination predicate if any and check its consistency *) diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 4a254d7910..2fe22364d5 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -164,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let term = Termops.it_mkLambda_or_LetIn def ctx in term, termtype in - let termtype = Evarutil.nf_isevar !evars termtype in - let term = Evarutil.nf_isevar !evars term in + let termtype = Evarutil.nf_evar !evars termtype in + let term = Evarutil.nf_evar !evars term in evars := undefined_evars !evars; Evarutil.check_evars env Evd.empty !evars termtype; let hook vis gr = diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 1bc3dbb345..3c907962ce 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -456,8 +456,8 @@ module Coercion = struct let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly - (Some (nf_isevar evd cj.uj_val)) - (nf_isevar evd cj.uj_type) (nf_isevar evd t) + (Some (nf_evar evd cj.uj_val)) + (nf_evar evd cj.uj_type) (nf_evar evd t) with NoCoercion -> let sigma = evd in try diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 8a7d11d1d8..d93a4b695e 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -50,7 +50,7 @@ open Subtac_obligations (* Functions to parse and interpret constructions *) let evar_nf isevars c = - Evarutil.nf_isevar !isevars c + Evarutil.nf_evar !isevars c let interp_gen kind isevars env ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) @@ -213,7 +213,7 @@ let telescope = function let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> - (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx + (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = Coqlib.check_required_library ["Coq";"Program";"Wf"]; @@ -318,7 +318,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let _ = isevars := Evarutil.nf_evar_map !isevars in let binders_rel = nf_evar_context !isevars binders_rel in let binders = nf_evar_context !isevars binders in - let top_arity = Evarutil.nf_isevar !isevars top_arity in + let top_arity = Evarutil.nf_evar !isevars top_arity in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in @@ -326,7 +326,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ce = - { const_entry_body = Evarutil.nf_isevar !isevars body; + { const_entry_body = Evarutil.nf_evar !isevars body; const_entry_type = Some ty; const_entry_opaque = false; const_entry_boxed = false} @@ -345,8 +345,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = Impargs.declare_manual_implicits false gr impls in hook, recname, typ in - let fullcoqc = Evarutil.nf_isevar !isevars def in - let fullctyp = Evarutil.nf_isevar !isevars typ in + let fullcoqc = Evarutil.nf_evar !isevars def in + let fullctyp = Evarutil.nf_evar !isevars typ in let evm = evars_of_term !isevars Evd.empty fullctyp in let evm = evars_of_term !isevars evm fullcoqc in let evm = non_instanciated_map env isevars evm in diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index a59cb96652..5b42c8ba5f 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -125,7 +125,7 @@ let subtac_process env isevars id bl c tycon = let imps = Option.default (Implicit_quantifiers.implicits_of_rawterm ~with_products:false c) imps in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars !isevars in - let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in + let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in evm, coqc, ty, imps open Subtac_obligations -- cgit v1.2.3