diff options
| author | Pierre-Marie Pédrot | 2016-01-11 22:20:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-14 18:23:32 +0100 |
| commit | 448866f0ec5291d58677d8fccbefde493ade0ee2 (patch) | |
| tree | 2824618cc31f7422be33f537c4ae8a8719180c53 /parsing | |
| parent | 67b9b34d409c793dc449104525684852353ee064 (diff) | |
Removing constr generic argument.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index df0d262062..3ed5304251 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -272,7 +272,7 @@ let create_entry u s etyp = new_entry etyp u s let create_constr_entry s = - outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType) + outGramObj (rawwit wit_constr) (create_entry uconstr s (unquote (rawwit wit_constr))) let create_generic_entry s wit = outGramObj wit (create_entry utactic s (unquote wit)) @@ -633,7 +633,7 @@ let compute_entry allow_create adjust forpat = function let u = get_univ u in let e = try get_entry u n - with Not_found when allow_create -> create_entry u n ConstrArgType in + with Not_found when allow_create -> create_entry u n (unquote (rawwit wit_constr)) in object_of_typed_entry e, None, true (* This computes the name of the level where to add a new rule *) |