diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
| commit | 7e2f953c3c19904616c43990fada92e762aadec9 (patch) | |
| tree | 8268d6e2b66ccdcce69df129ed98703e87f141b0 /plugins/subtac/subtac_cases.ml | |
| 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 'plugins/subtac/subtac_cases.ml')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 29ce9d3d4..491b44fbb 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 *) |