Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

6 files changed, 33 insertions, 29 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9ef782ff..a1860329 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 9617 2007-02-07 18:59:26Z herbelin $ *)
+(* $Id: command.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -111,7 +111,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv DEFAULTcast,comtyp)) bl in
+	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in
 	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
@@ -699,8 +699,8 @@ let save id const (locality,kind) hook =
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   Pfedit.delete_current_proof ();
-  hook l r;
-  definition_message id
+  definition_message id;
+  hook l r
 
 let save_named opacity =
   let id,(const,persistence,hook) = Pfedit.cook_proof () in
@@ -736,8 +736,8 @@ let admit () =
   let kn =
     declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
-  hook Global (ConstRef kn);
-  assumption_message id
+  assumption_message id;
+  hook Global (ConstRef kn)
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 6f9a55c3..e043f354 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: command.mli 9110 2006-09-01 12:30:52Z herbelin $ i*)
+(*i $Id: command.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -36,6 +36,9 @@ val declare_definition : identifier -> definition_kind ->
 
 val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 
+val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> 
+  Names.variable located -> unit
+
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
 
@@ -52,6 +55,8 @@ val build_scheme : (identifier located * bool * reference * rawsort) list -> uni
 
 val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+
 val start_proof : identifier -> goal_kind -> constr ->
   declaration_hook -> unit
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index dc2cc8cd..1809baa5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml 9528 2007-01-24 09:43:03Z herbelin $ *)
+(* $Id: himsg.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -331,7 +331,7 @@ let explain_occur_check ctx ev rhs =
   str" with term" ++ brk(1,1) ++ pt
 
 let explain_hole_kind env = function
-  | QuestionMark -> str "a term for this placeholder"
+  | QuestionMark _ -> str "a term for this placeholder"
   | CasesType ->
       str "the type of this pattern-matching problem"
   | BinderType (Name id) ->
@@ -352,9 +352,8 @@ let explain_hole_kind env = function
 
 let explain_not_clean ctx ev t k =
   let ctx = make_all_name_different ctx in
-  let c = mkRel (Intset.choose (free_rels t)) in
   let id = Evd.string_of_existential ev in
-  let var = pr_lconstr_env ctx c in
+  let var = pr_lconstr_env ctx t in
   str"Tried to define " ++ explain_hole_kind ctx k ++
   str" (" ++ str id ++ str ")" ++ spc() ++
   str"with a term using variable " ++ var ++ spc () ++
@@ -381,15 +380,15 @@ let explain_wrong_case_info ctx ind ci =
     spc () ++ pc
        
 
-let explain_cannot_unify m n =
-  let pm = pr_lconstr m in 
-  let pn = pr_lconstr n in
+let explain_cannot_unify ctx m n =
+  let pm = pr_lconstr_env ctx m in 
+  let pn = pr_lconstr_env ctx n in
   str"Impossible to unify" ++ brk(1,1)  ++ pm ++ spc ()  ++
   str"with" ++ brk(1,1)  ++ pn
 
 let explain_cannot_unify_local env m n subn =
-  let pm = pr_lconstr m in 
-  let pn = pr_lconstr n in
+  let pm = pr_lconstr_env env m in 
+  let pn = pr_lconstr_env env n in
   let psubn = pr_lconstr_env env subn in
     str"Impossible to unify" ++ brk(1,1)  ++ pm ++ spc ()  ++
       str"with" ++ brk(1,1)  ++ pn ++ spc() ++ str"as" ++ brk(1,1) ++ 
@@ -402,9 +401,9 @@ let explain_refiner_cannot_generalize ty =
 let explain_no_occurrence_found c =
   str "Found no subterm matching " ++ pr_lconstr c ++ str " in the current goal"
 
-let explain_cannot_unify_binding_type m n =
-  let pm = pr_lconstr m in 
-  let pn = pr_lconstr n in
+let explain_cannot_unify_binding_type ctx m n =
+  let pm = pr_lconstr_env ctx m in 
+  let pn = pr_lconstr_env ctx n in
   str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ 
   str "which should be unifiable with" ++ brk(1,1) ++ pn
 
@@ -464,11 +463,11 @@ let explain_pretype_error ctx err =
       explain_unexpected_type ctx actual expected
   | NotProduct c ->
       explain_not_product ctx c
-  | CannotUnify (m,n) -> explain_cannot_unify m n
+  | CannotUnify (m,n) -> explain_cannot_unify ctx m n
   | CannotUnifyLocal (e,m,n,sn) -> explain_cannot_unify_local e m n sn
   | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
   | NoOccurrenceFound c -> explain_no_occurrence_found c
-  | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
+  | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type ctx m n
 
 (* Refiner errors *)
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index bf0271d9..ab430d0c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: record.ml 9082 2006-08-24 17:03:28Z herbelin $ *)
+(* $Id: record.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -36,10 +36,10 @@ let interp_decl sigma env = function
   | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
-	| Some t -> mkCastC (c, Rawterm.CastConv DEFAULTcast,t)
+	| Some t -> mkCastC (c, Rawterm.CastConv (DEFAULTcast,t))
       in
       let j = interp_constr_judgment Evd.empty env c in
-      (id,Some j.uj_val, j.uj_type)
+      (id,Some j.uj_val, refresh_universes j.uj_type)
 
 let typecheck_params_and_fields ps fs =
   let env0 = Global.env () in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 248e0106..fb719a21 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 9481 2007-01-11 19:17:56Z herbelin $ i*)
+(*i $Id: vernacentries.ml 9874 2007-06-04 13:46:11Z soubiran $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -395,7 +395,7 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o =
        let binders_ast,argsexport =
         List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
-           (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+           (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast
              ([],[]) in
 	Declaremods.start_module Modintern.interp_modtype export
 	  id binders_ast mty_ast_o;
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 042ee5c8..0e17df28 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: whelp.ml4 7837 2006-01-11 09:47:32Z herbelin $ *)
+(* $Id: whelp.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Options
 open Pp
@@ -139,11 +139,11 @@ let rec uri_of_constr c =
   | RLetIn (_,na,b,c) ->
       url_string "let "; url_of_name na; url_string "\\def ";
       uri_of_constr b; url_string " in "; uri_of_constr c
-  | RCast (_,c,_,t) ->
+  | RCast (_,c, CastConv (_,t)) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
   | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint"
-  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ ->
+  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"
   | RPatVar _ | RDynamic _ -> 
       anomaly "Found constructors not supported in constr") ()