From 01c7976340c59ee88e5f3b6c49a37a575efc9c4f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 8 May 2013 17:44:05 +0000
Subject: Share more information between constructors and arity of an inductive
 type in order to solve implicit arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16486 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Inductive.v | 8 ++++++++
 toplevel/command.ml            | 4 ++--
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index a63c99ebf9..3d4257543a 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -113,3 +113,11 @@ Inductive I A : A->Prop := C a : (forall A, A) -> I a.
 Inductive list (A : Set) : Set :=
   | nil : list A
   | cons : A -> list (A -> A) -> list A.
+
+(* Check inference of evars in arity using information from constructors *)
+
+Inductive foo1 : forall p, Prop := cc1 : foo1 0.
+
+(* Check cross inference of evars from constructors *)
+
+Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e3a2993400..6c69495c5f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -268,14 +268,14 @@ let prepare_param = function
   | (na,Some b,_) -> out_name na, LocalDef b
 
 let interp_ind_arity evdref env ind =
-  interp_type_evars_impls ~evdref env ind.ind_arity
+  interp_type_evars_impls ~evdref ~fail_evar:false env ind.ind_arity
 
 let interp_cstrs evdref env impls mldata arity ind =
   let cnames,ctyps = List.split ind.ind_lc in
   (* Complete conclusions of constructor types if given in ML-style syntax *)
   let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
   (* Interpret the constructor types *)
-  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref env ~impls) ctyps') in
+  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref ~fail_evar:false env ~impls) ctyps') in
     (cnames, ctyps'', cimpls)
 
 let interp_mutual_inductive (paramsl,indl) notations finite =
-- 
cgit v1.2.3