Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).

By the way, there is an open problem of which conversion to use (conv,
evarconv, with or w/o universes levels) when trying to unify multiple
instances of the same variable in ltac pattern-matching.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13130 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 29 insertions, 5 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2b050b7ebf..7f1993079e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1704,14 +1704,19 @@ let is_match_catchable = function
   | PatternMatchingFailure | Eval_fail _ -> true
   | e -> Logic.catchable_exception e
 
+let equal_instances gl (ctx',c') (ctx,c) =
+  (* How to compare instances? Do we want the terms to be convertible?
+     unifiable? Do we want the universe levels to be relevant? 
+     (historically, conv_x is used) *)
+  ctx = ctx' & pf_conv_x gl c' c
+
 (* Verifies if the matched list is coherent with respect to lcm *)
 (* While non-linear matching is modulo eq_constr in matches, merge of *)
 (* different instances of the same metavars is here modulo conversion... *)
 let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
   let rec aux = function
-  | (id,(ctx,c) as x)::tl ->
-      if List.for_all
-	(fun (id',(ctx',c')) -> id'<>id or ctx = ctx' & pf_conv_x gl c' c) lcm
+  | (id,c as x)::tl ->
+      if List.for_all (fun (id',c') -> id'<>id or equal_instances gl c' c) lcm
       then
 	x :: aux tl
       else
@@ -1755,7 +1760,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
                  match_next_pattern find_next')
               with
                 | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
-            match_next_pattern (fun () -> match_pat lmatch hyp pat) ()
+            match_next_pattern (fun () ->
+	      let hyp = if b<>None then refresh_universes_strict hyp else hyp in
+	      match_pat lmatch hyp pat) ()
 	| Some patv ->
 	    match b with
 	    | Some body ->
@@ -1771,7 +1778,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
                         | PatternMatchingFailure ->
                             match_next_pattern_in_body next_in_body' () in
                     match_next_pattern_in_typ
-                      (fun () -> match_pat lmeta hyp pat) ()
+                      (fun () ->
+			let hyp = refresh_universes_strict hyp in
+			match_pat lmeta hyp pat) ()
                   with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
                 in
                 match_next_pattern_in_body
diff --git a/test-suite/bugs/closed/shouldsucceed/2300.v b/test-suite/bugs/closed/shouldsucceed/2300.v
new file mode 100644
index 0000000000..4e587cbb25
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2300.v
@@ -0,0 +1,15 @@
+(* Check some behavior of Ltac pattern-matching wrt universe levels *)
+
+Section contents.
+
+Variables (A: Type) (B: (unit -> Type) -> Type).
+
+Inductive C := c: A -> unit -> C.
+
+Let unused2 (x: unit) := C.
+
+Goal True.
+intuition.
+Qed.
+
+End contents.