diff options
| author | herbelin | 2010-06-29 08:27:03 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-29 08:27:03 +0000 |
| commit | 7e2f953c3c19904616c43990fada92e762aadec9 (patch) | |
| tree | 8268d6e2b66ccdcce69df129ed98703e87f141b0 /tactics | |
| parent | ee711f8994d5e2e94cc61292ac6aab125c23df1c (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 8 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 |
2 files changed, 9 insertions, 7 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 12a14eb014..a0d0027e42 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1006,12 +1006,12 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let cstrevars = !evars in let evars = solve_constraints env cstrevars in let p = map_rewprf - (fun p -> nf_zeta env evars (Evarutil.nf_isevar evars p)) + (fun p -> nf_zeta env evars (Evarutil.nf_evar evars p)) p in - let newt = Evarutil.nf_isevar evars newt in + let newt = Evarutil.nf_evar evars newt in let abs = Option.map (fun (x, y) -> - Evarutil.nf_isevar evars x, Evarutil.nf_isevar evars y) abs in + Evarutil.nf_evar evars x, Evarutil.nf_evar evars y) abs in let undef = split_evars (fst cstrevars) evars in let rewtac = match is_hyp with @@ -1422,7 +1422,7 @@ let build_morphism_signature m = mkApp (Lazy.force proper_type, [| t; sig_; m |]) in let evd = solve_constraints env !isevars in - let m = Evarutil.nf_isevar evd morph in + let m = Evarutil.nf_evar evd morph in Evarutil.check_evars env Evd.empty evd m; m let default_morphism sign m = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0be1e08fc6..9f5c611234 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2470,7 +2470,7 @@ let specialize_eqs id gl = let acc' = it_mkLambda_or_LetIn acc ctx'' in let ty' = Tacred.whd_simpl env !evars ty' and acc' = Tacred.whd_simpl env !evars acc' in - let ty' = Evarutil.nf_isevar !evars ty' in + let ty' = Evarutil.nf_evar !evars ty' in if worked then tclTHENFIRST (Tacmach.internal_cut true id ty') (exact_no_check (refresh_universes_strict acc')) gl @@ -3463,8 +3463,10 @@ let abstract_subproof id tac gl = global_sign (empty_named_context,empty_named_context_val) in let id = next_global_ident_away id (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in - if occur_existential concl then - error "\"abstract\" cannot handle existentials."; + let concl = + try flush_and_check_evars (project gl) concl + with Uninstantiated_evar _ -> + error "\"abstract\" cannot handle existentials." in let const = Pfedit.build_constant_by_tactic secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in |