summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/command.ml12
-rw-r--r--toplevel/command.mli7
-rw-r--r--toplevel/himsg.ml27
-rw-r--r--toplevel/record.ml6
-rw-r--r--toplevel/vernacentries.ml4
-rw-r--r--toplevel/whelp.ml46
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") ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 18:04:19 +0000