From b4f2e48b9e128a62d63668621844b571d3449cbf Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 30 Mar 2015 11:13:41 +0200
Subject: grammar: export hypident

This is necessary to make ssr compile with both camlp4/5
---
 interp/constrarg.ml  | 3 +++
 interp/constrarg.mli | 2 ++
 2 files changed, 5 insertions(+)

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 3f232c3612..a7241399e0 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -55,6 +55,9 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
 
 let wit_bindings = unsafe_of_type BindingsArgType
 
+let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
+  Genarg.make0 None "hyp_location_flag"
+
 let wit_red_expr = unsafe_of_type RedExprArgType
 
 let wit_clause_dft_concl  =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 74c6bd310c..fdeddd66a1 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -64,6 +64,8 @@ val wit_bindings :
   glob_constr_and_expr bindings,
   constr bindings Evd.sigma) genarg_type
 
+val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
+
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
-- 
cgit v1.2.3