comment out GProj in order to make #8456 pass CI

LPCIC · Oct 18, 2018 · 083cf0d · 083cf0d
1 parent 58f22cb
commit 083cf0d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
@@ -102,7 +102,7 @@ let rec gterm2lp depth state x = match (DAst.get x) (*.CAst.v*) with
 
   | GEvar(_k,_subst) -> nYI "(glob)HOAS for GEvar"
   | GPatVar _ -> nYI "(glob)HOAS for GPatVar"
-  | GProj _ -> nYI "(glob)HOAS for GProj"
+(*   | GProj _ -> nYI "(glob)HOAS for GProj" *)
 
   | GApp(hd,args) ->
       let state, hd = gterm2lp depth state hd in