Imported Upstream version 8.3upstream/8.3

6 files changed, 84 insertions, 76 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index faf0482b..ca2f4916 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: auto.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: auto.ml 13390 2010-09-02 08:03:01Z herbelin $ *)
 
 open Pp
 open Util
@@ -706,12 +706,11 @@ let print_applicable_hint () =
 (* displays the whole hint database db *)
 let print_hint_db db =
   let (ids, csts) = Hint_db.transparent_state db in
-  msg (hov 0
+  msgnl (hov 0
 	  ((if Hint_db.use_dn db then str"Discriminated database"
-	    else str"Non-discriminated database") ++ fnl ()));
-  msg (hov 0
-	  (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++
-	   str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ()));
+	    else str"Non-discriminated database")));
+  msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids));
+  msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts));
   Hint_db.iter
     (fun head hintlist ->
       match head with
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 3e2191d1..825ec492 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_tactics.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: evar_tactics.ml 13428 2010-09-17 18:03:40Z herbelin $ *)
 
 open Term
 open Util
@@ -53,7 +53,8 @@ let instantiate n (ist,rawc) ido gl =
         gl
 
 let let_evar name typ gls =
-  let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) typ in
+  let src = (dummy_loc,GoalEvar) in
+  let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in
   Refiner.tclTHEN (Refiner.tclEVARS sigma')
     (Tactics.letin_tac None name evar None nowhere) gls
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e1ac42c2..3f069ab2 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *)
 
 open Pp
 open Pcoq
@@ -624,3 +624,8 @@ TACTIC EXTEND hget_evar
 END
 
 (**********************************************************************)
+
+TACTIC EXTEND constr_eq
+| [ "constr_eq" constr(x) constr(y) ] -> [ 
+    if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ]
+END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 9d99ad96..d8497a7d 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -431,29 +431,30 @@ let pointwise_or_dep_relation n t car rel =
 	  [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |])
 
 let lift_cstr env sigma evars (args : constr list) ty cstr =
-  let cstr =
-    let start env car =
-      match cstr with
-      | None | Some (_, None) ->
-	  Evarutil.e_new_evar evars env (mk_relation car)
-      | Some (ty, Some rel) -> rel
-    in
-    let rec aux env prod n = 
-      if n = 0 then start env prod
-      else
-	match kind_of_term (Reduction.whd_betadeltaiota env prod) with
-	| Prod (na, ty, b) ->
-	    if noccurn 1 b then
-	      let b' = lift (-1) b in
-	      let rb = aux env b' (pred n) in
-		mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |])
-	    else
-	      let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) in
-		mkApp (Lazy.force forall_relation, 
-		      [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |])
-	| _ -> assert false
-    in aux env ty (List.length args)
-  in Some (ty, cstr)
+  let start env car =
+    match cstr with
+    | None | Some (_, None) ->
+	Evarutil.e_new_evar evars env (mk_relation car)
+    | Some (ty, Some rel) -> rel
+  in
+  let rec aux env prod n args = 
+    if n = 0 then Some (start env prod)
+    else
+      match kind_of_term (Reduction.whd_betadeltaiota env prod) with
+      | Prod (na, ty, b) ->
+	  if noccurn 1 b then
+	    let b' = lift (-1) b in
+	    let rb = aux env b' (pred n) (List.tl args) in
+	      Option.map (fun rb -> mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |]))
+		rb
+	  else
+	    let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) (List.tl args) in
+	      Option.map 
+		(fun rb -> mkApp (Lazy.force forall_relation, 
+				  [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]))
+		rb
+      | _ -> None
+  in Option.map (fun rel -> (ty, rel)) (aux env ty (List.length args) args)
 
 let unlift_cstr env sigma = function
   | None -> None
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 95e44c40..ba9a5173 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 13360 2010-07-30 08:47:08Z herbelin $ *)
+(* $Id: tacinterp.ml 13489 2010-10-03 22:27:12Z herbelin $ *)
 
 open Constrintern
 open Closure
@@ -401,8 +401,10 @@ let intern_ltac_variable ist = function
       raise Not_found
 
 let intern_constr_reference strict ist = function
-  | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
-      RVar (dloc,id), None
+  | Ident (_,id) as r when not strict & find_hyp id ist ->
+      RVar (dloc,id), Some (CRef r)
+  | Ident (_,id) as r when find_ctxvar id ist ->
+      RVar (dloc,id), if strict then None else Some (CRef r)
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
@@ -564,9 +566,10 @@ let intern_evaluable_reference_or_by_notation ist = function
 (* Globalize a reduction expression *)
 let intern_evaluable ist = function
   | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
-  | AN (Ident (_,id)) when
-      (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
-      ArgArg (EvalVarRef id, None)
+  | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist ->
+      ArgArg (EvalVarRef id, Some (loc,id))
+  | AN (Ident (loc,id)) when find_ctxvar id ist ->
+      ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id))
   | r ->
       let e = intern_evaluable_reference_or_by_notation ist r in
       let na = short_name r in
@@ -1138,7 +1141,8 @@ let interp_hyp ist gl (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.")
+  else user_err_loc (loc,"eval_variable",
+    str "No such hypothesis: " ++ pr_id id ++ str ".")
 
 let hyp_list_of_VList env = function
   | VList l -> List.map (coerce_to_hyp env) l
@@ -1210,7 +1214,7 @@ let interp_evaluable ist env = function
        with Not_found ->
        match r with
        | EvalConstRef _ -> r
-       | _ -> Pretype_errors.error_var_not_found_loc loc id)
+       | _ -> error_global_not_found_loc (loc,qualid_of_ident id))
   | ArgArg (r,None) -> r
   | ArgVar locid ->
       interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
@@ -1616,8 +1620,9 @@ let interp_induction_arg ist gl sigma arg =
   let env = pf_env gl in
   match arg with
   | ElimOnConstr c ->
-      let sigma, c = interp_constr_with_bindings ist env sigma c in
-      sigma, ElimOnConstr c
+      let sigma', (c,b) = interp_constr_with_bindings ist env sigma c in
+      let sigma, c = solve_remaining_evars false true env sigma sigma' c in
+      sigma, ElimOnConstr (c,b)
   | ElimOnAnonHyp n as x -> sigma, x
   | ElimOnIdent (loc,id) ->
       try
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9e4be0af..4ecc4739 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: tactics.ml 13464 2010-09-24 22:23:02Z herbelin $ *)
 
 open Pp
 open Util
@@ -868,13 +868,18 @@ type conjunction_status =
   | DefinedRecord of constant option list
   | NotADefinedRecordUseScheme of constr
 
-let make_projection params cstr sign elim i n c =
+let make_projection sigma params cstr sign elim i n c =
   let elim = match elim with
   | NotADefinedRecordUseScheme elim ->
       let (na,b,t) = List.nth cstr.cs_args i in
       let b = match b with None -> mkRel (i+1) | Some b -> b in
       let branch = it_mkLambda_or_LetIn b cstr.cs_args in
-      if noccur_between 1 (n-i-1) t then
+      if
+	(* excludes dependent projection types *)
+	noccur_between 1 (n-i-1) t
+	(* excludes flexible projection types *)
+	&& not (isEvar (fst (whd_betaiota_stack sigma t)))
+      then
         let t = lift (i+1-n) t in
 	Some (beta_applist (elim,params@[t;branch]),t)
       else
@@ -883,7 +888,8 @@ let make_projection params cstr sign elim i n c =
       match List.nth l i with
       | Some proj ->
 	  let t = Typeops.type_of_constant (Global.env()) proj in
-	  Some (beta_applist (mkConst proj,params),prod_applist t (params@[c]))
+	  let args = extended_rel_vect 0 sign in
+	  Some (beta_applist (mkConst proj,params),prod_applist t (params@[mkApp (c,args)]))
       | None -> None
   in Option.map (fun (abselim,elimt) -> 
     let c = beta_applist (abselim,[mkApp (c,extended_rel_vect 0 sign)]) in
@@ -908,7 +914,7 @@ let descend_in_conjunctions tac exit c gl =
 	    NotADefinedRecordUseScheme elim in
 	tclFIRST
 	  (list_tabulate (fun i gl ->
-	    match make_projection params cstr sign elim i n c with
+	    match make_projection (project gl) params cstr sign elim i n c with
 	    | None -> tclFAIL 0 (mt()) gl
 	    | Some (p,pt) ->
 	    tclTHENS
@@ -2188,6 +2194,8 @@ let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
 let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
 let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
 
+let coq_block = lazy (Coqlib.coq_constant "tactics" ["Program";"Equality"] "block")
+
 let mkEq t x y = 
   mkApp (Lazy.force coq_eq, [| refresh_universes_strict t; x; y |])
     
@@ -2303,23 +2311,6 @@ let hyps_of_vars env sign nogen hyps =
         sign 
     in lh
 
-exception Seen
-
-let linear vars args = 
-  let seen = ref vars in
-    try 
-      Array.iter (fun i -> 
-	let rels = ids_of_constr ~all:true Idset.empty i in
-	let seen' = 
-	  Idset.fold (fun id acc ->
-	    if Idset.mem id acc then raise Seen
-	    else Idset.add id acc)
-	    rels !seen
-	in seen := seen')
-	args;
-      true
-    with Seen -> false
-
 let is_defined_variable env id =
   pi2 (lookup_named id env) <> None
 
@@ -2373,19 +2364,23 @@ let abstract_args gl generalize_vars dep id defined f args =
 	    nongenvars, Idset.union argvars vars, env)
   in 
   let f', args' = decompose_indapp f args in
+  let parvars = ids_of_constr ~all:true Idset.empty f' in
   let dogen, f', args' =
-    let parvars = ids_of_constr ~all:true Idset.empty f' in
-      if not (linear parvars args') then true, f, args
-      else
-	match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with
-	| None -> false, f', args'
-	| Some nonvar ->
-	    let before, after = array_chop nonvar args' in
-	      true, mkApp (f', before), after
+    let seen = ref parvars in
+    let find i x = not (isVar x) || 
+      let v = destVar x in
+	if is_defined_variable env v || Idset.mem v !seen then true
+	else (seen := Idset.add v !seen; false)
+    in
+      match array_find_i find args' with
+      | None -> false, f', args'
+      | Some nonvar ->
+	  let before, after = array_chop nonvar args' in
+	    true, mkApp (f', before), after
   in
     if dogen then
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = 
-	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,Idset.empty,env) args'
+	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],parvars,Idset.empty,env) args'
       in
       let args, refls = List.rev args, List.rev refls in
       let vars = 
@@ -2440,14 +2435,14 @@ let specialize_eqs id gl =
     match kind_of_term ty with
     | Prod (na, t, b) -> 
 	(match kind_of_term t with
-	| App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
+	| App (eq, [| eqty; x; y |]) when in_eqs && eq_constr eq (Lazy.force coq_eq) ->
 	    let c = if noccur_between 1 (List.length ctx) x then y else x in
 	    let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
 	    let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
 	      if unif (push_rel_context ctx env) evars pt t then
 		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
 	      else acc, in_eqs, ctx, ty
-	| App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
+	| App (heq, [| eqty; x; eqty'; y |]) when in_eqs && eq_constr heq (Lazy.force coq_heq) ->
 	    let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in
 	    let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
 	    let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
@@ -2459,8 +2454,10 @@ let specialize_eqs id gl =
 	    else 
 	      let e = e_new_evar evars (push_rel_context ctx env) t in
 		aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
+    | App (f, args) when eq_constr f (Lazy.force coq_block) && not in_eqs ->
+	aux true ctx acc args.(1)
     | t -> acc, in_eqs, ctx, ty
-  in 
+  in
   let acc, worked, ctx, ty = aux false [] (mkVar id) ty in
   let ctx' = nf_rel_context_evar !evars ctx in
   let ctx'' = List.map (fun (n,b,t as decl) ->