diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-19 16:54:25 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-19 16:54:25 +0000 |
| commit | 38ff8d2b59a481ba489400ea194fdd78c6c2d5e1 (patch) | |
| tree | b0c539c86860a372b7356e6245e8db4fa50df16a /toplevel | |
| parent | 293675b06262698ba3b1ba30db8595bedd5c55ae (diff) | |
Add a parameter to QuestionMark evar kind to say it can be turned into an obligations (even an opaque one).
Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/command.mli | 3 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 | ||||
| -rw-r--r-- | toplevel/whelp.ml4 | 4 |
5 files changed, 8 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 739a7b47f..ecd0a6d7e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -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; diff --git a/toplevel/command.mli b/toplevel/command.mli index c4ef92447..9540888dd 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -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 diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 305685cc7..49a1d07f7 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -329,7 +329,7 @@ let explain_occur_check env 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) -> diff --git a/toplevel/record.ml b/toplevel/record.ml index f3ec4732d..b339d493b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -36,7 +36,7 @@ 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) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index eb9fdae30..b41bcec8b 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -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") () |