diff options
| author | herbelin | 2012-11-17 03:09:23 +0000 |
|---|---|---|
| committer | herbelin | 2012-11-17 03:09:23 +0000 |
| commit | 35846ec22445e14cb044ef3beb62f5c559d94752 (patch) | |
| tree | 283e8cc0a05b3f1722dadaabc900341ee63499ed /toplevel | |
| parent | beca7a2c11d6521bd9eec7bb0eb5d77a345f99ef (diff) | |
Taking into account the type of a definition (if it exists), and the
type in "cast" to activate the temporary interpretation scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 4 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 1a61982eac..c3ca35fe58 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -313,10 +313,10 @@ let rec find_pattern nt xl = function find_pattern nt (x::xl) (l,l') | [], NonTerminal x' :: l' -> (out_nt nt,x',List.rev xl),l' - | _, Terminal s :: _ | Terminal s :: _, _ -> - error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") + | _, Terminal s :: _ | Terminal s :: _, _ -> + error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") | _, [] -> error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> diff --git a/toplevel/record.ml b/toplevel/record.ml index 3332558a88..85abcc01ce 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -26,7 +26,7 @@ open Constrexpr_ops (********** definition d'un record (structure) **************) let interp_evars evdref env impls k typ = - let typ' = intern_gen true ~impls !evdref env typ in + let typ' = intern_gen Pretyping.IsType ~impls !evdref env typ in let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in imps, Pretyping.understand_tcc_evars evdref env k typ' |