From 0cc6076e7d4d92c1d899d450b2336dadbeb5f1b1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 25 Apr 2008 18:07:44 +0000
Subject: Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
 des théorèmes prouvés par récursion ou corécursion mutuelle.

Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml  | 8 ++++----
 pretyping/evarutil.mli | 4 ++++
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d80fdac9da..1701a84c93 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -226,10 +226,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	and f2 i =
           if sp1 = sp2 then
             ise_and i
-            [(fun i -> ise_array2 i
-                (fun i -> evar_conv_x env i CONV) al1 al2);
-             (fun i -> ise_list2 i
-                 (fun i -> evar_conv_x env i CONV) l1 l2)]
+            [(fun i -> ise_list2 i 
+                  (fun i -> evar_conv_x env i CONV) l1 l2);
+             (fun i -> solve_refl evar_conv_x env i sp1 al1 al2,
+                  true)]
           else (i,false)
 	in 
 	ise_try evd [f1; f2]
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7df11d3326..c5a3cbe3be 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -71,6 +71,10 @@ val non_instantiated : evar_map -> (evar * evar_info) list
 (* Unification utils *)
 
 val is_ground_term :  evar_defs -> constr -> bool
+val solve_refl : 
+  (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
+  -> env ->  evar_defs -> existential_key -> constr array -> constr array ->
+    evar_defs
 val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
   -> env ->  evar_defs -> conv_pb * existential * constr ->
-- 
cgit v1.2.3