From cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Dec 2015 02:08:42 +0100
Subject: Removing the special status of open_constr generic argument.

We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.
---
 grammar/argextend.ml4 | 1 -
 grammar/q_coqast.ml4  | 1 -
 2 files changed, 2 deletions(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 87a0dfa984..f6c223b741 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -33,7 +33,6 @@ let rec make_wit loc = function
   | IdentArgType -> <:expr< Constrarg.wit_ident >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
-  | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
   | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
   | PairArgType (t1,t2) ->
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index fc08f0a492..494ec6ba29 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -225,7 +225,6 @@ let mlexpr_of_red_expr = function
 let rec mlexpr_of_argtype loc = function
   | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
-  | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
   | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
-- 
cgit v1.2.3