Merge branch 'v8.5'

26 files changed, 537 insertions, 89 deletions

diff --git a/.gitignore b/.gitignore
index 54b9d10b5..c0bae6c66 100644
--- a/.gitignore
+++ b/.gitignore
@@ -160,3 +160,6 @@ dev/myinclude
 
 # coqide generated files (when testing)
 *.crashcoqide
+/doc/refman/Reference-Manual.hoptind
+/doc/refman/Reference-Manual.optidx
+/doc/refman/Reference-Manual.optind
diff --git a/CHANGES b/CHANGES
index 712a8a7e9..e44fd5de0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -83,10 +83,13 @@ Specification Language
 - Added a syntax $(...)$ that allows putting tactics in terms (may
   break user notations using "$(", fixable by inserting a space or
   rewriting the notation).
-- Constants in pattern-matching branches now respect the same rules regarding
-  implicit arguments than in applicative position. The old behavior can be
-  recovered by the command "Set Asymmetric Patterns". (possible source of
-  incompatibilities)
+- Constructors in pattern-matching patterns now respect the same rules
+  regarding implicit arguments than in applicative position. The old
+  behavior can be recovered by the command "Set Asymmetric
+  Patterns". As a side effect, Much more notations can be used in
+  patterns. Considering that the pattern language is rich enough like
+  that, definitions are now always forbidden in patterns. (source of
+  incompatibilities for definitions that delta-reduce to a constructor)
 - Type inference algorithm now granting opacity of constants. This might also
   affect behavior of tactics (source of incompatibilities, solvable by
   re-declaring transparent constants which were set opaque).
diff --git a/configure.ml b/configure.ml
index e83ebc7af..e8ef3ace7 100644
--- a/configure.ml
+++ b/configure.ml
@@ -534,6 +534,16 @@ let camltag = match caml_version_list with
 
 (** * CamlpX configuration *)
 
+(* Convention: we use camldir as a prioritary location for camlpX, if given *)
+
+let which_camlpX base =
+  match !Prefs.camldir with
+  | Some dir ->
+    let file = Filename.concat dir base in
+    if is_executable file then file else which base
+  | None ->
+    which base
+
 (* TODO: camlp5dir should rather be the *binary* location, just as camldir *)
 (* TODO: remove the late attempts at finding gramlib.cma *)
 
@@ -569,12 +579,12 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
 
 let check_camlp5_version () =
   try
-    let camlp5o = which "camlp5o" in
+    let camlp5o = which_camlpX "camlp5o" in
     let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
     let version = List.nth (string_split ' ' version_line) 2 in
     match string_split '.' version with
     | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) ->
-      printf "You have Camlp5 %s. Good!\n" version; camlp5o
+      printf "You have Camlp5 %s. Good!\n" version; camlp5o, version
     | _ -> failwith "bad version"
   with
   | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n"
@@ -585,8 +595,8 @@ let config_camlpX () =
     if not !Prefs.usecamlp5 then raise NoCamlp5;
     let camlp5mod = "gramlib" in
     let camlp5libdir = check_camlp5 (camlp5mod^".cma") in
-    let camlp5o = check_camlp5_version () in
-    "camlp5", camlp5o, Filename.basename camlp5o, camlp5libdir, camlp5mod
+    let camlp5o, camlp5_version = check_camlp5_version () in
+    "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version
   with NoCamlp5 ->
     (* We now try to use Camlp4, either by explicit choice or
        by lack of proper Camlp5 installation *)
@@ -595,12 +605,13 @@ let config_camlpX () =
     if not (Sys.file_exists (camlp4libdir/camlp4mod^".cma")) then
       die "No Camlp4 installation found.\n";
     try
-      let camlp4orf = which "camlp4orf" in
-      ignore (run camlp4orf []);
-      "camlp4", camlp4orf, Filename.basename camlp4orf, camlp4libdir, camlp4mod
+      let camlp4orf = which_camlpX "camlp4orf" in
+      let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in
+      let camlp4_version = List.nth (string_split ' ' version_line) 2 in
+      "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version
     with _ -> die "No Camlp4 installation found.\n"
 
-let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod = config_camlpX ()
+let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod, camlpX_version = config_camlpX ()
 
 let shorten_camllib s =
   if starts_with s (camllib^"/") then
@@ -957,9 +968,11 @@ let print_summary () =
   pr "  Coq VM bytecode link flags  : %s\n" (String.concat " " vmbyteflags);
   pr "  Other bytecode link flags   : %s\n" custom_flag;
   pr "  OS dependent libraries      : %s\n" osdeplibs;
-  pr "  OCaml/Camlp4 version        : %s\n" caml_version;
-  pr "  OCaml/Camlp4 binaries in    : %s\n" camlbin;
+  pr "  OCaml version               : %s\n" caml_version;
+  pr "  OCaml binaries in           : %s\n" camlbin;
   pr "  OCaml library in            : %s\n" camllib;
+  pr "  %s version              : %s\n"     (String.capitalize camlpX) camlpX_version;
+  pr "  %s binaries in          : %s\n"     (String.capitalize camlpX) camlpXbindir;
   pr "  %s library in           : %s\n"     (String.capitalize camlpX) camlpXlibdir;
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 0e7b39c75..f48cf6abf 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -74,9 +74,9 @@ This command is used to start an interactive module named {\ident}.
 \item {\tt Include {\module}}
 
   Includes the content of {\module} in the current interactive
- module. Here {\module} can be a module expresssion or a module type
+ module. Here {\module} can be a module expression or a module type
  expression. If {\module} is a high-order module or module type
- expression then the system tries to instanciate {\module}
+ expression then the system tries to instantiate {\module}
  by the current interactive module.
 
 \item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6824c399e..ea9b2755f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -924,7 +924,7 @@ let rec knr info m stk =
         | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
+          (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a88778c73..5912f0a0c 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -113,24 +113,14 @@ let mk_open_instance id idc gl m t=
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
-  let rec aux n avoid=
-    if Int.equal n 0 then [] else
+  let rec aux n avoid env evmap decls =
+    if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id avoid var_id gl) in
-	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
-  let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] env evmap nt in
-  let rec raux n t=
-    if Int.equal n 0 then t else
-      match t with
-	  GLambda(loc,name,k,_,t0)->
-	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1)
-	| _-> anomaly (Pp.str "can't happen") in
-  let ntt=try
-    fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)
-  with e when Errors.noncritical e ->
-    error "Untypable instance, maybe higher-order non-prenex quantification" in
-    decompose_lam_n_assum m ntt
+      let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+      let decl = (Name nid,None,c) in
+	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+  let evmap, decls = aux m [] env evmap [] in
+    evmap, decls, revt
 
 (* tactics   *)
 
@@ -159,11 +149,15 @@ let left_instance_tac (inst,id) continue seq=
 	    if m>0 then
 	      pf_constr_of_global id (fun idc ->
 		fun gl->
-		  let (rc,ot) = mk_open_instance id idc gl m t in
+		  let evmap,rc,ot = mk_open_instance id idc gl m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
-		    generalize [gt] gl)
+		  let evmap, _ =
+		    try Typing.e_type_of (pf_env gl) evmap gt
+		    with e when Errors.noncritical e ->
+		      error "Untypable instance, maybe higher-order non-prenex quantification" in
+		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
 		generalize [mkApp(idc,[|t|])])
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 637e0e28d..2a2ef30fb 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
   in
   aux bodyi
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 616ceeabd..f388f9005 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
-      let evd, b = 
-	try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 
-	with Univ.UniverseInconsistency _ -> evd, false
+      let evd, e = 
+	try
+	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
+	    env evd term1 term2 
+	  in
+	    if b then evd, None
+	    else evd, Some (ConversionFailed (env,term1,term2))
+	with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e)
       in
-	if b then Some (evd, true)
-	else if is_ground_env evd env then Some (evd, false)
-	else None)
+	match e with
+	| None -> Some (evd, e)
+	| Some e -> 
+	  if is_ground_env evd env then Some (evd, Some e)
+	  else None)
     else None
   in
   match ground_test with
-    | Some (evd, true) -> Success evd
-    | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2))
+    | Some (evd, None) -> Success evd
+    | Some (evd, Some e) -> UnifFailure (evd,e)
     | None ->
 	(* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f355d9a72..bfd19c6c7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -179,23 +179,30 @@ let restrict_instance evd evk filter argsv =
 
 let noccur_evar env evd evk c =
   let cache = ref Int.Set.empty (* cache for let-ins *) in
-  let rec occur_rec k c =
+  let rec occur_rec (k, env as acc) c =
   match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
-       | Some c -> occur_rec k c
+       | Some c -> occur_rec acc c
        | None ->
            if Evar.equal evk evk' then raise Occur
-           else Array.iter (occur_rec k) args')
+           else Array.iter (occur_rec acc) args')
   | Rel i when i > k ->
       if not (Int.Set.mem (i-k) !cache) then
-      (match pi2 (Environ.lookup_rel (i-k) env) with
+      (match pi2 (Environ.lookup_rel i env) with
        | None -> ()
-       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b))
-  | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c [])
-  | _ -> iter_constr_with_binders succ occur_rec k c
+       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
+  | Proj (p,c) -> 
+    let c = 
+      try Retyping.expand_projection env evd p c []
+      with Retyping.RetypeError _ -> 
+	(* Can happen when called from w_unify which doesn't assign evars/metas 
+	   eagerly enough *) c
+    in occur_rec acc c
+  | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
+    occur_rec acc c
   in
-  try occur_rec 0 c; true with Occur -> false
+  try occur_rec (0,env) c; true with Occur -> false
 
 (***************************************)
 (* Managing chains of local definitons *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c49bec9ae..009b7323e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with
 
 let pattern_of_constr env sigma t =
   let ctx = ref [] in
+  let keep = ref Evar.Set.empty in
+  let remove = ref Evar.Set.empty in
   let rec pattern_of_constr env t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -141,28 +143,35 @@ let pattern_of_constr env sigma t =
     | App (f,a) ->
         (match
           match kind_of_term f with
-            Evar (evk,args as ev) ->
-              (match snd (Evd.evar_source evk sigma) with
-                  Evar_kinds.MatchingVar (true,id) ->
-                    ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-                    Some id
-                | _ -> None)
-            | _ -> None
-          with
-            | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
-            | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
+          | Evar (evk,args as ev) ->
+            (match snd (Evd.evar_source evk sigma) with
+              Evar_kinds.MatchingVar (true,id) ->
+		let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+                  ctx := (id,None,ty)::!ctx;
+		  keep := Evar.Set.union (evars_of_term ty) !keep;
+		  remove := Evar.Set.add evk !remove;
+                  Some id
+            | _ -> None)
+          | _ -> None
+         with
+         | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
+         | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
     | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
       pattern_of_constr env (Retyping.expand_projection env sigma p c [])
     | Evar (evk,ctxt as ev) ->
-        (match snd (Evd.evar_source evk sigma) with
-          | Evar_kinds.MatchingVar (b,id) ->
-              ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-              assert (not b); PMeta (Some id)
-          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt)
-          | _ -> PMeta None)
+      remove := Evar.Set.add evk !remove;
+      (match snd (Evd.evar_source evk sigma) with
+      | Evar_kinds.MatchingVar (b,id) ->
+	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+          ctx := (id,None,ty)::!ctx;
+	  keep := Evar.Set.union (evars_of_term ty) !keep;
+          assert (not b); PMeta (Some id)
+      | Evar_kinds.GoalEvar -> 
+	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+      | _ -> PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
@@ -178,9 +187,11 @@ let pattern_of_constr env sigma t =
     | Fix f -> PFix f
     | CoFix f -> PCoFix f in
   let p = pattern_of_constr env t in
+  let remove = Evar.Set.diff !remove !keep in
+  let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in
   (* side-effect *)
   (* Warning: the order of dependencies in ctx is not ensured *)
-  (!ctx,p)
+  (sigma,!ctx,p)
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -220,7 +231,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  snd (pattern_of_constr env sigma c)
+	  pi3 (pattern_of_constr env sigma c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -245,7 +256,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 snd (pattern_of_constr (Global.env()) Evd.empty t)
+	 pi3 (pattern_of_constr (Global.env()) Evd.empty t)
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cf02421c2..9e72280fe 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> 
+  Evd.evar_map * named_context * constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 09eb38bd1..dd671f111 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -994,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
 	  reduce_and_refold_cofix whrec env cst_l cofix stack
 	|_ -> fold ()
       else fold ()
@@ -1073,7 +1073,7 @@ let local_whd_state_gen flags sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
 	  whrec (contract_cofix cofix, stack)
 	|_ -> s
       else s
@@ -1293,7 +1293,8 @@ let sigma_univ_state =
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
+let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
+    env sigma x y = 
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1315,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
-  | Univ.UniverseInconsistency _ -> sigma, false
+  | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d4f061c5b..1df2a73b2 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 
 (** [infer_fconv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
+    @raises UniverseInconsistency iff catch_incon is set to false, 
+    otherwise returns false in that case.
  *)
-val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> 
-  evar_map * bool
+val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
+  env -> evar_map -> constr -> constr -> evar_map * bool
 
 (** {6 Special-Purpose Reduction Functions } *)
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5621c365a..101223b57 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -609,7 +609,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = snd (Patternops.pattern_of_constr env sigma cty) in
+	let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -628,7 +628,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = snd (Patternops.pattern_of_constr env ce.evd c') in
+	let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -726,7 +726,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
+              pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
 	      name = name;
               code=Res_pf_THEN_trivial_fail(c,t,ctx) })
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8826875a3..1429211f1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -681,7 +681,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
 let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
   let p = match a with
   | Inl b -> Inl (interp_evaluable ist env sigma b)
-  | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in
+  | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
   interp_occurrences ist occs, p
 
 let interp_constr_with_occurrences_and_name_as_list =
@@ -1030,7 +1030,7 @@ let use_types = false
 
 let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
-    snd (interp_typed_pattern ist env sigma c)
+    pi3 (interp_typed_pattern ist env sigma c)
   else
     instantiate_pattern env sigma lfun pat
 
@@ -2138,7 +2138,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
-          let sign,op = interp_typed_pattern ist env sigma op in
+          let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
 	  let env' = Environ.push_named_context sign env in
           let c_interp sigma =
@@ -2146,8 +2146,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	      with e when to_catch e (* Hack *) ->
 		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
           in
-	      (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
-		gl
+	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
+	      { gl with sigma = sigma }
         end
       end
       end
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
new file mode 100644
index 000000000..80695f382
--- /dev/null
+++ b/test-suite/bugs/closed/3513.v
@@ -0,0 +1,75 @@
+(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
+Require Coq.Setoids.Setoid.
+Import Coq.Setoids.Setoid.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+Local Existing Instance ILFun_Ops.
+Local Existing Instance ILFun_ILogic.
+Definition catOP (P Q: OPred) : OPred := admit.
+Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
+admit.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end; unfold Basics.flip.
+  2: solve [ apply reflexivity ].
+  Undo.
+  2: reflexivity. (* Toplevel input, characters 18-29:
+Error:
+Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v
new file mode 100644
index 000000000..51d6744c5
--- /dev/null
+++ b/test-suite/bugs/closed/3590.v
@@ -0,0 +1,14 @@
+(* Set Primitive Projections. *)
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Definition idS := Set.
+Goal forall x y : prod Set Set, fst x = fst y.
+  intros.
+  change (@fst _ _ ?z) with (@fst Set idS z) at 2.
+  Unshelve.
+  admit.
+Qed.
+  
+(* Toplevel input, characters 20-58:
+Error: Failed to get enough information from the left-hand side to type the
+right-hand side. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
new file mode 100644
index 000000000..4069e3807
--- /dev/null
+++ b/test-suite/bugs/closed/3690.v
@@ -0,0 +1,52 @@
+Set Printing Universes.
+Set Universe Polymorphism.
+Definition foo (a := Type) (b := Type) (c := Type) := Type.
+Print foo.
+(* foo =
+let a := Type@{Top.1} in
+let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
+     : Type@{Top.4+1}
+(* Top.1
+   Top.2
+   Top.3
+   Top.4 |=  *) *)
+Check @foo. (* foo@{Top.5 Top.6 Top.7
+Top.8}
+     : Type@{Top.8+1}
+(* Top.5
+   Top.6
+   Top.7
+   Top.8 |=  *) *)
+Definition bar := $(let t := eval compute in foo in exact t)$.
+Check @bar. (* bar@{Top.13 Top.14 Top.15
+Top.16}
+     : Type@{Top.16+1}
+(* Top.13
+   Top.14
+   Top.15
+   Top.16 |=  *) *)
+(* The following should fail, since [bar] should only need one universe. *)
+Check @bar@{i j}.
+Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
+Definition qux := Eval compute in baz.
+Check @qux. (* qux@{Top.24 Top.25
+Top.26}
+     : Type@{max(Top.24+1, Top.26+1)}
+(* Top.24
+   Top.25
+   Top.26 |= Top.25 < Top.24
+              Top.26 < Top.25
+               *) *)
+Print qux. (* qux =
+Type@{Top.21} -> Type@{Top.23}
+     : Type@{max(Top.21+1, Top.23+1)}
+(* Top.21
+   Top.22
+   Top.23 |= Top.22 < Top.21
+              Top.23 < Top.22
+               *) *)
+Fail Check @qux@{Set Set}.
+Fail Check @qux@{Set Set Set}.
+(* [qux] should only need two universes *)
+Check @qux@{i j k}.  (* Error: The command has not failed!, but I think this is suboptimal *)
+Fail Check @qux@{i j}.
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v
new file mode 100644
index 000000000..6e5952a52
--- /dev/null
+++ b/test-suite/bugs/closed/3732.v
@@ -0,0 +1,104 @@
+(* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
+Require Coq.Lists.List.
+
+Import Coq.Lists.List.
+
+Set Implicit Arguments.
+Global Set Asymmetric Patterns.
+
+Section machine.
+  Variables pc state : Type.
+
+  Inductive propX (i := pc) (j := state) : list Type -> Type :=
+  | Inj : forall G, Prop -> propX G
+  | ExistsX : forall G A, propX (A :: G) -> propX G.
+
+  Implicit Arguments Inj [G].
+
+  Definition PropX := propX nil.
+  Fixpoint last (G : list Type) : Type.
+    exact (match G with
+             | nil => unit
+             | T :: nil => T
+             | _ :: G' => last G'
+           end).
+  Defined.
+  Fixpoint eatLast (G : list Type) : list Type.
+    exact (match G with
+             | nil => nil
+             | _ :: nil => nil
+             | x :: G' => x :: eatLast G'
+           end).
+  Defined.
+
+  Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) :=
+    match p with
+      | Inj _ P => fun _ => Inj P
+      | ExistsX G A p1 => fun p' =>
+                            match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with
+                              | nil => fun p1 _ => ExistsX p1
+                              | _ :: _ => fun _ rc => ExistsX rc
+                            end p1 (subst p1 (match G return (last G -> PropX) -> last (A :: G) -> PropX with
+                                                | nil => fun _ _ => Inj True
+                                                | _ => fun p' => p'
+                                              end p'))
+    end.
+
+  Definition spec := state -> PropX.
+  Definition codeSpec := pc -> option spec.
+
+  Inductive valid (specs : codeSpec) (G : list PropX) : PropX -> Prop := Env : forall P, In P G -> valid specs G P.
+  Definition interp specs := valid specs nil.
+End machine.
+Notation "'ExX' : A , P" := (ExistsX (A := A) P) (at level 89) : PropX_scope.
+Bind Scope PropX_scope with PropX propX.
+Variables pc state : Type.
+
+Inductive subs : list Type -> Type :=
+| SNil : subs nil
+| SCons : forall T Ts, (last (T :: Ts) -> PropX pc state) -> subs (eatLast (T :: Ts)) -> subs (T :: Ts).
+
+Fixpoint SPush G T (s : subs G) (f : T -> PropX pc state) : subs (T :: G) :=
+  match s in subs G return subs (T :: G) with
+    | SNil => SCons _ nil f SNil
+    | SCons T' Ts f' s' => SCons T (T' :: Ts) f' (SPush s' f)
+  end.
+
+Fixpoint Substs G (s : subs G) : propX pc state G -> PropX pc state :=
+  match s in subs G return propX pc state G -> PropX pc state with
+    | SNil => fun p => p
+    | SCons _ _ f s' => fun p => Substs s' (subst p f)
+  end.
+Variable specs : codeSpec pc state.
+
+Lemma simplify_fwd_ExistsX : forall G A s (p : propX pc state (A :: G)),
+                               interp specs (Substs s (ExX  : A, p))
+                               -> exists a, interp specs (Substs (SPush s a) p).
+admit.
+Defined.
+
+Goal    forall (G : list Type) (A : Type) (p : propX pc state (@cons Type A G))
+               (s : subs G)
+               (_ : @interp pc state specs (@Substs G s (@ExistsX pc state G A p)))
+               (P : forall _ : subs (@cons Type A G), Prop)
+               (_ : forall (s0 : subs (@cons Type A G))
+                           (_ : @interp pc state specs (@Substs (@cons Type A G) s0 p)),
+                      P s0),
+          @ex (forall _ : A, PropX pc state)
+              (fun a : forall _ : A, PropX pc state => P (@SPush G A s a)).
+  intros ? ? ? ? H ? H'.
+  apply simplify_fwd_ExistsX in H.
+  firstorder. 
+Qed.
+ (* Toplevel input, characters 15-19:
+Error: Illegal application:
+The term "cons" of type "forall A : Type, A -> list A -> list A"
+cannot be applied to the terms
+ "Type" : "Type"
+ "T" : "Type"
+ "G0" : "list Type"
+The 2nd term has type "Type@{Top.53}" which should be coercible to
+ "Type@{Top.12}".
+ *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4046.v b/test-suite/bugs/closed/4046.v
new file mode 100644
index 000000000..8f8779b7b
--- /dev/null
+++ b/test-suite/bugs/closed/4046.v
@@ -0,0 +1,6 @@
+Module Import Foo.
+  Class Foo := { foo : Type }.
+End Foo.
+
+Instance f : Foo := { foo := nat }. (* works fine *)
+Instance f' : Foo.Foo := { Foo.foo := nat }. 
diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v
new file mode 100644
index 000000000..2109a4cd9
--- /dev/null
+++ b/test-suite/bugs/closed/4097.v
@@ -0,0 +1,64 @@
+(* File reduced by coq-bug-finder from original input, then from 6082 lines to 81 lines, then from 436 lines to 93 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 27 2015 15:10:37 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (fc1b3ef9d7270938cd83c524aae0383093b7a4b5) *)
+Global Set Primitive Projections.
+Record sigT {A} (P : A -> Type) := exist { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} _ / .
+Arguments projT2 {A P} _ / .
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope path_scope.
+Open Scope fibration_scope.
+Notation "( x ; y )" := (exist _ _ x y) : fibration_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
+  p # (f x) = f y
+  :=
+  match p with idpath => idpath end.
+Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
+  (p : x = y) (z : P (f x))
+  : transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+admit.
+Defined.
+Generalizable Variables X A B C f g n.
+Definition pr1_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+: u.1 = v.1
+  := ap pr1 p.
+Notation "p ..1" := (pr1_path p) (at level 3) : fibration_scope.
+Definition pr2_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+: p..1 # u.2 = v.2
+  := (transport_compose P pr1 p u.2)^
+     @ (@apD {x:A & P x} _ pr2 _ _ p).
+Notation "p ..2" := (pr2_path p) (at level 3) : fibration_scope.
+Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2})
+: p = q.
+admit.
+Defined.
+Set Debug Unification.
+Definition path_path_sigma {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (r : p..1 = q..1)
+           (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2)
+: p = q
+  := path_path_sigma_uncurried P u v p q (r; s).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v
new file mode 100644
index 000000000..a38b05096
--- /dev/null
+++ b/test-suite/bugs/closed/4101.v
@@ -0,0 +1,19 @@
+(* File reduced by coq-bug-finder from original input, then from 10940 lines to 152 lines, then from 509 lines to 163 lines, then from 178 lines to 66 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 2 2015 18:53:10 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (e77f178e60918f14eacd1ec0364a491d4cfd0f3f) *)
+
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x),
+                      (forall x, f x = g x) -> f = g.
+Lemma sigT_obj_eq
+: forall (T : Type) (T0 : T -> Type)
+         (s s0 : forall s : sigT T0,
+                   sigT (fun _ : T0 (projT1 s) => unit) ->
+                   sigT (fun _ : T0 (projT1 s) => unit)),
+   s0 = s.
+Proof.
+  intros.
+  Set Debug Tactic Unification.
+  apply path_forall. 
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4103.v b/test-suite/bugs/closed/4103.v
new file mode 100644
index 000000000..92cc0279a
--- /dev/null
+++ b/test-suite/bugs/closed/4103.v
@@ -0,0 +1,12 @@
+Set Primitive Projections.
+
+CoInductive stream A := { hd : A; tl : stream A }.
+
+CoFixpoint ticks (n : nat) : stream unit := {| hd := tt; tl := ticks n |}.
+
+Lemma expand : exists n : nat, (ticks n) = (ticks n).(tl _).
+Proof.
+  eexists.
+  (* Set Debug Tactic Unification. *)
+  (* Set Debug RAKAM. *)
+  reflexivity.
diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v
new file mode 100644
index 000000000..99ca6cb39
--- /dev/null
+++ b/test-suite/bugs/opened/3794.v
@@ -0,0 +1,7 @@
+Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate.
+Hint Unfold not : core.
+
+Goal true<>false.
+Set Typeclasses Debug.
+Fail typeclasses eauto with core.
+Abort.
\ No newline at end of file
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
new file mode 100644
index 000000000..4e0b7bf5c
--- /dev/null
+++ b/test-suite/success/coindprim.v
@@ -0,0 +1,52 @@
+Set Primitive Projections.
+
+CoInductive stream A := { hd : A; tl : stream A }.
+
+CoFixpoint ticks : stream unit :=
+  {| hd := tt; tl := ticks |}.
+
+Arguments hd [ A ] s.
+Arguments tl [ A ] s.
+
+CoInductive bisim {A} : stream A -> stream A -> Prop :=
+  | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'.
+
+Lemma bisim_refl {A} (s : stream A) : bisim s s.
+Proof.
+  revert s.
+  cofix aux. intros. constructor. reflexivity. apply aux.
+Defined.
+
+Lemma constr : forall (A : Type) (s : stream A),
+    bisim s (Build_stream _ s.(hd) s.(tl)).
+Proof.
+  intros. constructor. reflexivity. simpl. apply bisim_refl.
+Defined.
+
+Lemma constr' : forall (A : Type) (s : stream A),
+  s = Build_stream _ s.(hd) s.(tl).
+Proof.
+  intros. 
+  Fail destruct s. 
+Abort.
+
+Eval compute in constr _ ticks.
+
+Notation convertible x y := (eq_refl x : x = y).
+
+Fail Check convertible ticks {| hd := hd ticks; tl := tl ticks |}.
+
+CoInductive U := inU
+ { outU : U }.
+
+CoFixpoint u : U :=
+  inU u.
+
+CoFixpoint force (u : U) : U :=
+  inU (outU u).
+
+Lemma eq (x : U) : x = force x.
+Proof.
+  Fail destruct x.
+Abort.
+  (* Impossible *)
\ No newline at end of file
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 93df848de..1e0bfacf9 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -330,6 +330,7 @@ let clean sds sps =
   if !some_vfile then
     begin
       print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n";
+      print "\tfind . -name .coq-native -type d -empty -delete\n";
       print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"
     end;
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
@@ -366,7 +367,7 @@ let implicit () =
     print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n";
     print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
-    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let ml_rules () =
     print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
     print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n";