From 49c842d98c3d32016a279f97497876c79cba9880 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 13 Jul 2004 13:35:42 +0000
Subject: 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
---
 proofs/clenv.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d3c835be43..cc7ab87107 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"))
-- 
cgit v1.2.3