diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-13 13:35:42 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-13 13:35:42 +0000 |
| commit | 49c842d98c3d32016a279f97497876c79cba9880 (patch) | |
| tree | a21ea44f70db88003a3e20d2f06bb6ec26d6a470 /proofs | |
| parent | 080869c96afe453dc49589ad47a3d0dcdc25f9a5 (diff) | |
bugs #667 and #783 (mimick_evar and loc_table on large files)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5894 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d3c835be4..cc7ab8710 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -534,6 +534,11 @@ let applyHead n c wc = in apprec n c (w_type_of wc c) wc +let is_mimick_head f = + match kind_of_term f with + (Const _|Var _|Rel _|Construct _|Ind _) -> true + | _ -> false + let rec mimick_evar hdc nargs sp wc = let evd = Evd.map wc.sigma sp in let wc' = extract_decl sp wc in @@ -571,7 +576,7 @@ and w_resrec metas evars wc = w_resrec metas t (w_Define evn rhs wc) with ex when catchable_exception ex -> (match krhs with - | App (f,cl) when isConst f -> + | App (f,cl) when is_mimick_head f -> let wc' = mimick_evar f (Array.length cl) evn wc in w_resrec metas evars wc' | _ -> raise ex (* error "w_Unify" *))) @@ -624,12 +629,12 @@ let clenv_merge with_types metas evars clenv = (clenv_wtactic (w_Define evn rhs') clenv) with ex when catchable_exception ex -> (match krhs with - | App (f,cl) when isConst f or isConstruct f -> + | App (f,cl) when is_mimick_head f -> clenv_resrec metas evars (clenv_wtactic (mimick_evar f (Array.length cl) evn) clenv) - | _ -> raise ex(********* error "w_Unify" *)) + | _ -> raise ex (* error "w_Unify" *)) end | _ -> anomaly "clenv_resrec")) |