diff options
| author | delahaye | 2001-10-02 21:47:46 +0000 |
|---|---|---|
| committer | delahaye | 2001-10-02 21:47:46 +0000 |
| commit | f7a91c9c1b323e2b15b3d7ae427ad0dd3dd8bf51 (patch) | |
| tree | 70b85be5fcb2dfd57ce38926d69623f9bf7c9792 /pretyping/rawterm.ml | |
| parent | 5e5d618bc8e642f0052dd5b99d5db97a452b8284 (diff) | |
Ajout de dynamiques pour les quotations constr et tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/rawterm.ml')
| -rw-r--r-- | pretyping/rawterm.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 053c6c39b7..a46a3f8b5b 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -56,6 +56,7 @@ type rawconstr = | RSort of loc * rawsort | RHole of loc option | RCast of loc * rawconstr * rawconstr + | RDynamic of loc * Dyn.t (*i - if PRec (_, names, arities, bodies) is in env then arities are @@ -87,6 +88,7 @@ let loc_of_rawconstr = function | RHole (Some loc) -> loc | RHole (None) -> dummy_loc | RCast (loc,_,_) -> loc + | RDynamic (loc,_) -> loc let set_loc_of_rawconstr loc = function | RRef (_,a) -> RRef (loc,a) @@ -103,9 +105,6 @@ let set_loc_of_rawconstr loc = function | RSort (_,a) -> RSort (loc,a) | RHole _ -> RHole (Some loc) | RCast (_,a,b) -> RCast (loc,a,b) + | RDynamic (_,d) -> RDynamic (loc,d) let join_loc (deb1,_) (_,fin2) = (deb1,fin2) - - - - |